\begin{tabbing}
ma{-}ef{-}const($M$;$k$;$x$;$s$;$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(\=product{-}deq(Knd;Id;KindDeq;IdDeq);\+
\\[0ex](($M$.2.2.2.2).1);
\\[0ex]$<$$k$, $x$$>$;
\\[0ex]${\it kx}$,$E$.constant\_function($E$($s$,$v$);$\mathbb{Q}$;$M$.ds($x$)))
\-
\end{tabbing}